The
is printed from the input
verbatim13#
The formula
For algebraic-style proofs, there is the
Here, again, is the input:
verbatim14#
When the left-hand side is long, I find this style better than the LATEX
Another brand of box is the inference rule; the rule
comes from the input
verbatim15#
Note the optional argument to
Finally, there's the
from input like this:
verbatim16#
This kind of thing is useful when you're describing a language, and it can also be used for data-type definitions. I've even---time for a confession---used it once for a fragment of VDM. The final column is optional: just omit the third